\begin{tabbing}
R{-}interface{-}compat($A$;$B$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if \=Rsends?($B$)$\rightarrow$\+\+
\\[0ex]i\=f \=Reffect?($A$)$\rightarrow$\+\+
\\[0ex]let $k$ = Reffect{-}knd($A$) in 
\\[0ex]if isrcv($k$) $\wedge_{2}$ lnk($k$) = Rsends{-}l($B$)$\rightarrow$ Rsends{-}dt($B$)(tag($k$))?Void $\subseteq\rho$ Reffect{-}T($A$)
\\[0ex]else True fi
\-\\[0ex]; \=Rsends?($A$)$\rightarrow$\+
\\[0ex]let $k$ = Rsends{-}knd($A$) in 
\\[0ex]if isrcv($k$) $\wedge_{2}$ lnk($k$) = Rsends{-}l($B$)$\rightarrow$ Rsends{-}dt($B$)(tag($k$))?Void $\subseteq\rho$ Rsends{-}T($A$)
\\[0ex]else True fi
\-\-\\[0ex]else True fi
\-\\[0ex]else True fi
\-
\end{tabbing}